#include "minizincmodel.h"

#include <stdio.h>
#include <stack>
#include <iostream>

#include "minizincvariable.h"
#include "schemacomponentformula.h"
#include "formula.h"
#include "columnReference.h"
#include "logicUnaryOperation.h"
#include "logicBinaryOperation.h"
#include "numericBinaryOperation.h"
#include "numericUnaryOperation.h"
#include "symbolicVariable.h"
#include "substitution.h"

char* minInt =  NULL;
char* maxInt  = NULL;
using namespace std;

MiniZincModel::MiniZincModel(SchemaComponentFormula * formula)
{
	if(formula != NULL){
	  declarations = new set<MiniZincVariable*,set_object >();
	  output = new set<string>();
		inserts = new map< pair<string,int>,set<pair<string,string> > >();
		vector<Formula *> * all_formulas = formula->getAllFormulas();
		vector<Expression *> * all_formulas_formatted = new vector<Expression *>();
		for(unsigned int i=0; i<all_formulas->size(); i++){
			all_formulas_formatted->push_back(formatExpression(all_formulas->at(i)->getExpression()));

			vector<Substitution *> * substitutions = all_formulas->at(i)->getSubstitutions();
			for(unsigned int j=0; j<substitutions->size(); j++){
			    Expression * formatted_substitution = formatExpression(substitutions->at(j)->getSubstitution());
                output->insert("\" " + substitutions->at(j)->getSubstituted() + " =\" , show(" + formatted_substitution->toString() + ")");
                delete formatted_substitution; formatted_substitution = NULL;
			}// for

		}// for
	
	map<string, vector<BooleanExpression *> * > *  tableConstraints = formula->getTableConstraints();
		map<string, vector<BooleanExpression *> * >::iterator it;
		table_constraints = new map <string,Expression*>();
		for(it=tableConstraints->begin(); it!=tableConstraints->end(); it++){
		  const string tname = it->first;
		  Expression * e =formatExpression(createConjunction((*it).second));
		  table_constraints->insert(pair<string,Expression*>(tname,e));
		}
		constraint = createDisjunction(all_formulas_formatted);
		
		for(unsigned int i=0; i<all_formulas_formatted->size(); i++) delete all_formulas_formatted->at(i);
		delete all_formulas_formatted; all_formulas_formatted = NULL;
	}else{
		declarations = NULL;
		constraint = NULL;
		output = NULL;
		inserts = NULL;
	}// if-else
}

MiniZincModel::~MiniZincModel()
{
    delete declarations; declarations = NULL;
    delete constraint; constraint = NULL;
    delete output; output = NULL;
	delete inserts; inserts = NULL;
}

Expression * MiniZincModel::formatExpression(Expression * expression)
{
	Expression * result = expression->clone();
	Expression * pointer = result;

	SymbolicVariable * sv = dynamic_cast<SymbolicVariable *>(pointer);
	if(sv != NULL){
		
		MiniZincVariable * to_add = new MiniZincVariable(sv);
		declarations->insert(dynamic_cast<MiniZincVariable *>(to_add->clone()));
		delete result; result = NULL;
		result = to_add->clone();

		const string tname = (const string)sv->getTableName();
		const int row = sv->getRowIndex();
		const string cname=sv->getColumnName();
		const string toAddtoString=to_add->toOutputString();
		pair <string,int> key=make_pair(tname,row);
		map< pair<string,int>,set<pair<string,string> > >::iterator it;
		it = inserts->find(key);
		set< pair <string,string> > ins;
		if (it != inserts->end()) ins = (*it).second;
		pair<string,string> columnAndRepresentation = make_pair(cname,toAddtoString);
		ins.insert(columnAndRepresentation);
		inserts->erase(key);
		inserts->insert(pair<pair<string,int>,set<pair<string,string> > >(key,ins));
		
		delete to_add; to_add = NULL;
		return result;
	}//if

	stack<Expression *> lifo;
	lifo.push(pointer);
	while(!lifo.empty()){
		pointer = lifo.top();
		lifo.pop();
		LogicBinaryOperation * lbe = dynamic_cast<LogicBinaryOperation *>(pointer);
		if(lbe != NULL){
			if(lbe->getOperator() == "AND" || lbe->getOperator() == "and") lbe->setOperator("/\\");
			if(lbe->getOperator() == "OR" || lbe->getOperator() == "or" ) lbe->setOperator("\\/");
			if(lbe->getOperator() == "<=") lbe->setOperator("<=");
			if(lbe->getOperator() == "<") lbe->setOperator("<");
			if(lbe->getOperator() == ">=") lbe->setOperator(">=");
			if(lbe->getOperator() == ">") lbe->setOperator(">");
			if(lbe->getOperator() == "==") lbe->setOperator("=");
			if(lbe->getOperator() == "!=") lbe->setOperator("!=");

			//TODO string comparisson
			SymbolicVariable * svr = dynamic_cast<SymbolicVariable *>(lbe->getRightExpression());
			if(svr != NULL){
				MiniZincVariable * to_add = new MiniZincVariable(svr);
				declarations->insert(dynamic_cast<MiniZincVariable*>(to_add->clone()));
				lbe->setRightExpression(to_add);
				
				const string tname = (const string)svr->getTableName();
				const int row = svr->getRowIndex();
				const string cname=svr->getColumnName();
				const string toAddtoString=to_add->toOutputString();
				pair <string,int> key=make_pair(tname,row);
				map< pair<string,int>,set<pair<string,string> > >::iterator it;
				it = inserts->find(key);
				set< pair <string,string> > ins;
				if (it != inserts->end()) ins = (*it).second;
				pair<string,string> columnAndRepresentation = make_pair(cname,toAddtoString);
				ins.insert(columnAndRepresentation);
				inserts->erase(key);
				inserts->insert(pair<pair<string,int>,set<pair<string,string> > >(key,ins));
				
				delete to_add; to_add = NULL;
				
			}else{
				lifo.push(lbe->getRightExpression());
			}// if-else

			SymbolicVariable * svl = dynamic_cast<SymbolicVariable *>(lbe->getLeftExpression());
			if(svl != NULL){
				MiniZincVariable * to_add = new MiniZincVariable(svl);
				declarations->insert(dynamic_cast<MiniZincVariable *>(to_add->clone()));
				lbe->setLeftExpression(to_add->clone());
				
				const string tname = (const string)svl->getTableName();
				const int row = svl->getRowIndex();
				const string cname=svl->getColumnName();
				const string toAddtoString=to_add->toOutputString();
				pair <string,int> key=make_pair(tname,row);
				map< pair<string,int>,set<pair<string,string> > >::iterator it;
				it = inserts->find(key);
				set< pair <string,string> > ins;
				if (it != inserts->end()) ins = (*it).second;
				pair<string,string> columnAndRepresentation = make_pair(cname,toAddtoString);
				ins.insert(columnAndRepresentation);
				inserts->erase(key);
				inserts->insert(pair<pair<string,int>,set<pair<string,string> > >(key,ins));
				
				delete to_add; to_add = NULL;
				
			}else{
				lifo.push(lbe->getLeftExpression());
			}// if-else
		}else{
			LogicUnaryOperation * lue = dynamic_cast<LogicUnaryOperation *>(pointer);
			if(lue != NULL){
				if(lue->getOperator() == "NOT" || lue->getOperator() == "not") lue->setOperator("not");

				SymbolicVariable * sv = dynamic_cast<SymbolicVariable *>(lue->getExpression());
				if(sv != NULL){
					MiniZincVariable * to_add = new MiniZincVariable(sv);
					declarations->insert(dynamic_cast<MiniZincVariable *>(to_add->clone()));
					lue->setExpression(to_add->clone());
					
					const string tname = (const string)sv->getTableName();
					const int row = sv->getRowIndex();
					const string cname=sv->getColumnName();
					const string toAddtoString=to_add->toOutputString();
					pair <string,int> key=make_pair(tname,row);
					map< pair<string,int>,set<pair<string,string> > >::iterator it;
					it = inserts->find(key);
					set< pair <string,string> > ins;
					if (it != inserts->end()) ins = (*it).second;
					pair<string,string> columnAndRepresentation = make_pair(cname,toAddtoString);
					ins.insert(columnAndRepresentation);
					inserts->erase(key);
					inserts->insert(pair<pair<string,int>,set<pair<string,string> > >(key,ins));
					
					delete to_add; to_add = NULL;
					
				}else{
					lifo.push(lue->getExpression());
				}// if-else
			}else{
				NumericBinaryOperation * nbe = dynamic_cast<NumericBinaryOperation *>(pointer);
				if(nbe != NULL){
					if(nbe->getOperator() == "+") nbe->setOperator("+");
					if(nbe->getOperator() == "-") nbe->setOperator("-");
					if(nbe->getOperator() == "*") nbe->setOperator("*");
					if(nbe->getOperator() == "/") nbe->setOperator("/");

					SymbolicVariable * svr = dynamic_cast<SymbolicVariable *>(nbe->getRightExpression());
					if(svr != NULL){
						MiniZincVariable * to_add = new MiniZincVariable(svr);
						declarations->insert(dynamic_cast<MiniZincVariable *>(to_add->clone()));
						nbe->setRightExpression(to_add->clone());

						
						const string tname = (const string)svr->getTableName();
						const int row = svr->getRowIndex();
						const string cname=svr->getColumnName();
						const string toAddtoString=to_add->toOutputString();
						pair <string,int> key=make_pair(tname,row);
						map< pair<string,int>,set<pair<string,string> > >::iterator it;
						it = inserts->find(key);
						set< pair <string,string> > ins;
						if (it != inserts->end()) ins = (*it).second;
						pair<string,string> columnAndRepresentation = make_pair(cname,toAddtoString);
						ins.insert(columnAndRepresentation);
						inserts->erase(key);
						inserts->insert(pair<pair<string,int>,set<pair<string,string> > >(key,ins));
						
						delete to_add; to_add = NULL;
						
					}else{
						lifo.push(nbe->getRightExpression());
					}// if-else

					SymbolicVariable * svl = dynamic_cast<SymbolicVariable *>(nbe->getLeftExpression());
					if(svl != NULL){
						MiniZincVariable * to_add = new MiniZincVariable(svl);
						declarations->insert(dynamic_cast<MiniZincVariable *>(to_add->clone()));
						nbe->setLeftExpression(to_add->clone());
						
						const string tname = (const string)svl->getTableName();
						const int row = svl->getRowIndex();
						const string cname=svl->getColumnName();
						const string toAddtoString=to_add->toOutputString();
						pair <string,int> key=make_pair(tname,row);
						map< pair<string,int>,set<pair<string,string> > >::iterator it;
						it = inserts->find(key);
						set< pair <string,string> > ins;
						if (it != inserts->end()) ins = (*it).second;
						pair<string,string> columnAndRepresentation = make_pair(cname,toAddtoString);
						ins.insert(columnAndRepresentation);
						inserts->erase(key);
						inserts->insert(pair<pair<string,int>,set<pair<string,string> > >(key,ins));
						
						delete to_add; to_add = NULL;
						
					}else{
						lifo.push(nbe->getLeftExpression());
					}// if-else
				}else{
					NumericUnaryOperation * nue = dynamic_cast<NumericUnaryOperation *>(pointer);
					if(nue != NULL){
						if(nbe->getOperator() == "-") nbe->setOperator("-");

						SymbolicVariable * sv = dynamic_cast<SymbolicVariable *>(nue->getExpression());
						if(sv != NULL){
							MiniZincVariable * to_add = new MiniZincVariable(sv);
							declarations->insert(dynamic_cast<MiniZincVariable *>(to_add->clone()));
							nue->setExpression(to_add->clone());
							
							const string tname = (const string)sv->getTableName();
							const int row = sv->getRowIndex();
							const string cname=sv->getColumnName();
							const string toAddtoString=to_add->toOutputString();
							pair <string,int> key=make_pair(tname,row);
							map< pair<string,int>,set<pair<string,string> > >::iterator it;
							it = inserts->find(key);
							set< pair <string,string> > ins;
							if (it != inserts->end()) ins = (*it).second;
							pair<string,string> columnAndRepresentation = make_pair(cname,toAddtoString);
							ins.insert(columnAndRepresentation);
							inserts->erase(key);
							inserts->insert(pair<pair<string,int>,set<pair<string,string> > >(key,ins));
							
							delete to_add; to_add = NULL;
							
						}else{
							lifo.push(nue->getExpression());
						}// if-else
					}else{
						// NOTHING TO DO
					}// if-else
				}// if-else
			}// if-else
		}//if-else
	}// while

	return result;
}

Expression * MiniZincModel::createDisjunction(vector<Expression *> * expressions)
{
	if(expressions->size() == 1){
		return expressions->at(0)->clone();
	}// if

	LogicBinaryOperation * result = new LogicBinaryOperation(NULL,"\\/",NULL);
	Expression * pointer = result;
	for(int i=0; i<expressions->size()-1; i++){
		LogicBinaryOperation * casting = dynamic_cast<LogicBinaryOperation *>(pointer);
		casting->setLeftExpression(expressions->at(i));
		if(i == expressions->size()-2){
			casting->setRightExpression(expressions->at(i+1));
		}else{
			LogicBinaryOperation * aux = new LogicBinaryOperation(NULL,"\\/",NULL);
			casting->setRightExpression(aux);
			delete aux; aux = NULL;
		}// if-else
		pointer = casting->getRightExpression();
	}// for

	return result;
}

Expression * MiniZincModel::createConjunction(vector<BooleanExpression *> * expressions)
{
	if(expressions->size() == 1){
		return expressions->at(0)->clone();
	}// if

	LogicBinaryOperation * result = new LogicBinaryOperation(NULL,"/\\",NULL);
	Expression * pointer = result;
	for(int i=0; i<expressions->size()-1; i++){
		LogicBinaryOperation * casting = dynamic_cast<LogicBinaryOperation *>(pointer);
		casting->setLeftExpression(expressions->at(i));
		if(i == expressions->size()-2){
			casting->setRightExpression(expressions->at(i+1));
		}else{
			LogicBinaryOperation * aux = new LogicBinaryOperation(NULL,"/\\",NULL);
			casting->setRightExpression(aux);
			delete aux; aux = NULL;
		}// if-else
		pointer = casting->getRightExpression();
	}// for

	return result;
}

string MiniZincModel::toString()
{
  //TODO (stcgstring.mzn doesn't have to be in the current directory... change following include declaration)  
  string str ="";
  //  str = str + "include \"stcgstring.mzn\"; \n";
    str = str + "int: numChar=127;\n";
    set<MiniZincVariable*,set_object>::iterator it;
    if (minInt!=NULL || maxInt!=NULL){
		if (minInt!=NULL) str = str + "int: minInt = " + minInt + ";\n";
		else { 
			fprintf(stderr,"Warning, minimum integer value not specified. it have been set to -1000000000.\n"); 
			str = str + "int: minInt = " + "-1000000000" + ";\n";
		}
		if (maxInt!=NULL) str = str + "int: maxInt = " + maxInt + ";\n";
		else { 
			fprintf(stderr,"Warning, maximum integer value not specified, it have been set to 1000000000.\n"); 
			str = str + "int: maxInt = " + "1000000000" + ";\n";
		}    
		for(it=declarations->begin(); it!=declarations->end(); it++){
		MiniZincVariable* v = *it;
		  switch(v->getType().type){
		  case(INTEGER):
		    str = str + "var minInt..maxInt: " + (v->toString()) + ";\n";
		    break;
		  case(BOOLEAN):
		    str = str + "var bool: " + (v->toString()) + ";\n";
		    break;
			case(STRING):{
				str = str + "array[0..";
				char buffer [33];
				sprintf(buffer,"%d",v->getType().size);
				string str_length(buffer);
				str += str_length;
				str = str + "] of var 0..numChar: " + (v->toString()) + ";\n";
				break;
			}
		  default:
		    break;

		  }
		    
		}// for
	}
	
	else
		for(it=declarations->begin(); it!=declarations->end(); it++){
		  MiniZincVariable* v = *it;
		  switch(v->getType().type){
		  case(INTEGER):
		    str = str + "var int: " + (v->toString()) + ";\n";
		    break;
		  case(BOOLEAN):
		    str = str + "var bool: " + (v->toString()) + ";\n";
		    break;
			case(STRING):{
				str = str + "array[0..";
				char buffer [33];
				sprintf(buffer,"%d",v->getType().size);
				string str_length(buffer);
				str += str_length;
				str = str + "] of var 0..numChar: " + (v->toString()) + ";\n";
				break;
			}
		  default:
		    break;

		  }
		}// for
    map<string,Expression*>::iterator itc;
    for(itc=table_constraints->begin(); itc!=table_constraints->end(); itc++){
      str = str + "% Table constraints for table "+ (*itc).first + ":\n";
      str = str +"constraint "+ (*itc).second->toString() + ";\n";
    }

    str = str + "constraint " + constraint->toString() + ";\n";

    str = str + "solve satisfy;\n";

    str = str + "output [";
   /* for(it=output->begin(); it!=output->end(); it++){
        str = str + " " + (*it) + ",";
    }// for
    str.erase(str.length()-1);*/
    map< pair<string,int>,set<pair<string,string> > >::iterator it2;
	for (it2=inserts->begin();it2!=inserts->end();it2++){
		set< pair <string,string> > ins = (*it2).second ;
		pair <string,int> key = (*it2).first;
		set< pair <string,string> >::iterator it3;
		str = str + "\" INSERT INTO " + key.first+ " (";
		for (it3=ins.begin();it3!=ins.end();it3++){
			str = str + (*it3).first.c_str() + ",";
		}
		    str.erase(str.length()-1);
		str = str + ") VALUES (\"" ;
		for (it3=ins.begin();it3!=ins.end();it3++){
			str = str + ", "+(*it3).second+ ",\",\"";
		}
		str.erase(str.length()-4);
		str= str+ ",\");\\n\",";
	}
	str.erase(str.length()-1);	
	
    str = str + "];";
	
	
    return str;
}


